(set-option :produce-interpolants 1)
(set-option :certify-interpolants 1)
(set-logic QF_LRA)
(declare-fun |state_type::state.delta| () Real)
(declare-fun |state_type::state.v!0| () Real)
(declare-fun |state_type::state.v!1| () Real)
(declare-fun |state_type::state.v!2| () Real)
(declare-fun |state_type::state.v!3| () Real)
(declare-fun |state_type::state.v!4| () Real)
(declare-fun |state_type::state.p!0!0| () Real)
(declare-fun |state_type::state.p!0!1| () Real)
(declare-fun |state_type::state.p!0!2| () Real)
(declare-fun |state_type::state.p!0!3| () Real)
(declare-fun |state_type::state.p!0!4| () Real)
(declare-fun |state_type::state.p!1!0| () Real)
(declare-fun |state_type::state.p!1!1| () Real)
(declare-fun |state_type::state.p!1!2| () Real)
(declare-fun |state_type::state.p!1!3| () Real)
(declare-fun |state_type::state.p!1!4| () Real)
(declare-fun |state_type::state.p!2!0| () Real)
(declare-fun |state_type::state.p!2!1| () Real)
(declare-fun |state_type::state.p!2!2| () Real)
(declare-fun |state_type::state.p!2!3| () Real)
(declare-fun |state_type::state.p!2!4| () Real)
(declare-fun |state_type::state.p!3!0| () Real)
(declare-fun |state_type::state.p!3!1| () Real)
(declare-fun |state_type::state.p!3!2| () Real)
(declare-fun |state_type::state.p!3!3| () Real)
(declare-fun |state_type::state.p!3!4| () Real)
(declare-fun |state_type::state.p!4!0| () Real)
(declare-fun |state_type::state.p!4!1| () Real)
(declare-fun |state_type::state.p!4!2| () Real)
(declare-fun |state_type::state.p!4!3| () Real)
(declare-fun |state_type::state.p!4!4| () Real)
(declare-fun |state_type::state.round| () Real)
(declare-fun |state_type::state.status!0| () Real)
(declare-fun |state_type::state.status!1| () Real)
(declare-fun |state_type::state.status!2| () Real)
(declare-fun |state_type::state.status!3| () Real)
(declare-fun |state_type::state.status!4| () Real)
(declare-fun |state_type::state.n!0| () Real)
(declare-fun |state_type::state.n!1| () Real)
(declare-fun |state_type::state.n!2| () Real)
(declare-fun |state_type::state.n!3| () Real)
(declare-fun |state_type::state.n!4| () Real)
(assert (!
(and (and (> |state_type::state.delta| 0) (and (not (<= |state_type::state.v!0| 0)) (not (<= |state_type::state.v!1| 0)) (not (<= |state_type::state.v!2| 0)) (not (<= |state_type::state.v!3| 0)) (not (<= |state_type::state.v!4| 0)) (<= (- |state_type::state.v!0| |state_type::state.v!0|) |state_type::state.delta|) (<= (- |state_type::state.v!1| |state_type::state.v!0|) |state_type::state.delta|) (<= (- |state_type::state.v!2| |state_type::state.v!0|) |state_type::state.delta|) (<= (- |state_type::state.v!3| |state_type::state.v!0|) |state_type::state.delta|) (<= (- |state_type::state.v!4| |state_type::state.v!0|) |state_type::state.delta|) (<= (- |state_type::state.v!0| |state_type::state.v!1|) |state_type::state.delta|) (<= (- |state_type::state.v!1| |state_type::state.v!1|) |state_type::state.delta|) (<= (- |state_type::state.v!2| |state_type::state.v!1|) |state_type::state.delta|) (<= (- |state_type::state.v!3| |state_type::state.v!1|) |state_type::state.delta|) (<= (- |state_type::state.v!4| |state_type::state.v!1|) |state_type::state.delta|) (<= (- |state_type::state.v!0| |state_type::state.v!2|) |state_type::state.delta|) (<= (- |state_type::state.v!1| |state_type::state.v!2|) |state_type::state.delta|) (<= (- |state_type::state.v!2| |state_type::state.v!2|) |state_type::state.delta|) (<= (- |state_type::state.v!3| |state_type::state.v!2|) |state_type::state.delta|) (<= (- |state_type::state.v!4| |state_type::state.v!2|) |state_type::state.delta|) (<= (- |state_type::state.v!0| |state_type::state.v!3|) |state_type::state.delta|) (<= (- |state_type::state.v!1| |state_type::state.v!3|) |state_type::state.delta|) (<= (- |state_type::state.v!2| |state_type::state.v!3|) |state_type::state.delta|) (<= (- |state_type::state.v!3| |state_type::state.v!3|) |state_type::state.delta|) (<= (- |state_type::state.v!4| |state_type::state.v!3|) |state_type::state.delta|) (<= (- |state_type::state.v!0| |state_type::state.v!4|) |state_type::state.delta|) (<= (- |state_type::state.v!1| |state_type::state.v!4|) |state_type::state.delta|) (<= (- |state_type::state.v!2| |state_type::state.v!4|) |state_type::state.delta|) (<= (- |state_type::state.v!3| |state_type::state.v!4|) |state_type::state.delta|) (<= (- |state_type::state.v!4| |state_type::state.v!4|) |state_type::state.delta|)) (= |state_type::state.p!0!0| 1) (= |state_type::state.p!0!1| 2) (= |state_type::state.p!0!2| 3) (= |state_type::state.p!0!3| 4) (= |state_type::state.p!0!4| 5) (= |state_type::state.p!1!0| 1) (= |state_type::state.p!1!1| 2) (= |state_type::state.p!1!2| 3) (= |state_type::state.p!1!3| 4) (= |state_type::state.p!1!4| 5) (= |state_type::state.p!2!0| 1) (= |state_type::state.p!2!1| 2) (= |state_type::state.p!2!2| 3) (= |state_type::state.p!2!3| 4) (= |state_type::state.p!2!4| 5) (= |state_type::state.p!3!0| 1) (= |state_type::state.p!3!1| 2) (= |state_type::state.p!3!2| 3) (= |state_type::state.p!3!3| 4) (= |state_type::state.p!3!4| 5) (= |state_type::state.p!4!0| 1) (= |state_type::state.p!4!1| 2) (= |state_type::state.p!4!2| 3) (= |state_type::state.p!4!3| 4) (= |state_type::state.p!4!4| 5) (= |state_type::state.round| 0) (and (= |state_type::state.status!0| 4) (= |state_type::state.status!1| 2) (= |state_type::state.status!2| 0) (= |state_type::state.status!3| 0) (= |state_type::state.status!4| 0))) (and (or (= |state_type::state.p!0!0| 1) (= |state_type::state.p!0!0| 2) (= |state_type::state.p!0!0| 3) (= |state_type::state.p!0!0| 4) (= |state_type::state.p!0!0| 5)) (or (= |state_type::state.p!0!1| 1) (= |state_type::state.p!0!1| 2) (= |state_type::state.p!0!1| 3) (= |state_type::state.p!0!1| 4) (= |state_type::state.p!0!1| 5)) (or (= |state_type::state.p!0!2| 1) (= |state_type::state.p!0!2| 2) (= |state_type::state.p!0!2| 3) (= |state_type::state.p!0!2| 4) (= |state_type::state.p!0!2| 5)) (or (= |state_type::state.p!0!3| 1) (= |state_type::state.p!0!3| 2) (= |state_type::state.p!0!3| 3) (= |state_type::state.p!0!3| 4) (= |state_type::state.p!0!3| 5)) (or (= |state_type::state.p!0!4| 1) (= |state_type::state.p!0!4| 2) (= |state_type::state.p!0!4| 3) (= |state_type::state.p!0!4| 4) (= |state_type::state.p!0!4| 5)) (or (= |state_type::state.p!1!0| 1) (= |state_type::state.p!1!0| 2) (= |state_type::state.p!1!0| 3) (= |state_type::state.p!1!0| 4) (= |state_type::state.p!1!0| 5)) (or (= |state_type::state.p!1!1| 1) (= |state_type::state.p!1!1| 2) (= |state_type::state.p!1!1| 3) (= |state_type::state.p!1!1| 4) (= |state_type::state.p!1!1| 5)) (or (= |state_type::state.p!1!2| 1) (= |state_type::state.p!1!2| 2) (= |state_type::state.p!1!2| 3) (= |state_type::state.p!1!2| 4) (= |state_type::state.p!1!2| 5)) (or (= |state_type::state.p!1!3| 1) (= |state_type::state.p!1!3| 2) (= |state_type::state.p!1!3| 3) (= |state_type::state.p!1!3| 4) (= |state_type::state.p!1!3| 5)) (or (= |state_type::state.p!1!4| 1) (= |state_type::state.p!1!4| 2) (= |state_type::state.p!1!4| 3) (= |state_type::state.p!1!4| 4) (= |state_type::state.p!1!4| 5)) (or (= |state_type::state.p!2!0| 1) (= |state_type::state.p!2!0| 2) (= |state_type::state.p!2!0| 3) (= |state_type::state.p!2!0| 4) (= |state_type::state.p!2!0| 5)) (or (= |state_type::state.p!2!1| 1) (= |state_type::state.p!2!1| 2) (= |state_type::state.p!2!1| 3) (= |state_type::state.p!2!1| 4) (= |state_type::state.p!2!1| 5)) (or (= |state_type::state.p!2!2| 1) (= |state_type::state.p!2!2| 2) (= |state_type::state.p!2!2| 3) (= |state_type::state.p!2!2| 4) (= |state_type::state.p!2!2| 5)) (or (= |state_type::state.p!2!3| 1) (= |state_type::state.p!2!3| 2) (= |state_type::state.p!2!3| 3) (= |state_type::state.p!2!3| 4) (= |state_type::state.p!2!3| 5)) (or (= |state_type::state.p!2!4| 1) (= |state_type::state.p!2!4| 2) (= |state_type::state.p!2!4| 3) (= |state_type::state.p!2!4| 4) (= |state_type::state.p!2!4| 5)) (or (= |state_type::state.p!3!0| 1) (= |state_type::state.p!3!0| 2) (= |state_type::state.p!3!0| 3) (= |state_type::state.p!3!0| 4) (= |state_type::state.p!3!0| 5)) (or (= |state_type::state.p!3!1| 1) (= |state_type::state.p!3!1| 2) (= |state_type::state.p!3!1| 3) (= |state_type::state.p!3!1| 4) (= |state_type::state.p!3!1| 5)) (or (= |state_type::state.p!3!2| 1) (= |state_type::state.p!3!2| 2) (= |state_type::state.p!3!2| 3) (= |state_type::state.p!3!2| 4) (= |state_type::state.p!3!2| 5)) (or (= |state_type::state.p!3!3| 1) (= |state_type::state.p!3!3| 2) (= |state_type::state.p!3!3| 3) (= |state_type::state.p!3!3| 4) (= |state_type::state.p!3!3| 5)) (or (= |state_type::state.p!3!4| 1) (= |state_type::state.p!3!4| 2) (= |state_type::state.p!3!4| 3) (= |state_type::state.p!3!4| 4) (= |state_type::state.p!3!4| 5)) (or (= |state_type::state.p!4!0| 1) (= |state_type::state.p!4!0| 2) (= |state_type::state.p!4!0| 3) (= |state_type::state.p!4!0| 4) (= |state_type::state.p!4!0| 5)) (or (= |state_type::state.p!4!1| 1) (= |state_type::state.p!4!1| 2) (= |state_type::state.p!4!1| 3) (= |state_type::state.p!4!1| 4) (= |state_type::state.p!4!1| 5)) (or (= |state_type::state.p!4!2| 1) (= |state_type::state.p!4!2| 2) (= |state_type::state.p!4!2| 3) (= |state_type::state.p!4!2| 4) (= |state_type::state.p!4!2| 5)) (or (= |state_type::state.p!4!3| 1) (= |state_type::state.p!4!3| 2) (= |state_type::state.p!4!3| 3) (= |state_type::state.p!4!3| 4) (= |state_type::state.p!4!3| 5)) (or (= |state_type::state.p!4!4| 1) (= |state_type::state.p!4!4| 2) (= |state_type::state.p!4!4| 3) (= |state_type::state.p!4!4| 4) (= |state_type::state.p!4!4| 5)) (or (= |state_type::state.n!0| 0) (= |state_type::state.n!0| 1) (= |state_type::state.n!0| 2) (= |state_type::state.n!0| 3) (= |state_type::state.n!0| 4) (= |state_type::state.n!0| 5)) (or (= |state_type::state.n!1| 0) (= |state_type::state.n!1| 1) (= |state_type::state.n!1| 2) (= |state_type::state.n!1| 3) (= |state_type::state.n!1| 4) (= |state_type::state.n!1| 5)) (or (= |state_type::state.n!2| 0) (= |state_type::state.n!2| 1) (= |state_type::state.n!2| 2) (= |state_type::state.n!2| 3) (= |state_type::state.n!2| 4) (= |state_type::state.n!2| 5)) (or (= |state_type::state.n!3| 0) (= |state_type::state.n!3| 1) (= |state_type::state.n!3| 2) (= |state_type::state.n!3| 3) (= |state_type::state.n!3| 4) (= |state_type::state.n!3| 5)) (or (= |state_type::state.n!4| 0) (= |state_type::state.n!4| 1) (= |state_type::state.n!4| 2) (= |state_type::state.n!4| 3) (= |state_type::state.n!4| 4) (= |state_type::state.n!4| 5))))
:named a))


(assert (!
(and (= |state_type::state.p!0!0| 1) (= |state_type::state.p!1!0| 1) (= |state_type::state.p!2!0| 1) (= |state_type::state.p!3!0| 1) (= |state_type::state.p!4!0| 1) (= |state_type::state.p!0!1| 1) (= |state_type::state.p!0!2| 1) (= |state_type::state.p!0!3| 1) (= |state_type::state.p!0!4| 1) (= |state_type::state.p!1!1| 1) (= |state_type::state.p!1!2| 1) (= |state_type::state.p!1!3| 1) (= |state_type::state.p!1!4| 1) (= |state_type::state.p!2!1| 1) (= |state_type::state.p!2!2| 1) (= |state_type::state.p!2!3| 1) (= |state_type::state.p!2!4| 1) (= |state_type::state.p!3!1| 1) (= |state_type::state.p!3!2| 1) (= |state_type::state.p!3!3| 1) (= |state_type::state.p!3!4| 1) (= |state_type::state.p!4!1| 1) (= |state_type::state.p!4!2| 1) (= |state_type::state.p!4!3| 1) (= |state_type::state.p!4!4| 1) (= |state_type::state.n!0| 0) (= |state_type::state.n!1| 0) (= |state_type::state.n!2| 0) (= |state_type::state.n!3| 0) (= |state_type::state.n!4| 0) (not (>= (* (- 1) |state_type::state.status!1|) 0)) (= |state_type::state.v!0| 0) (= |state_type::state.v!3| 0) (not (>= (+ (- 3) (* 1 |state_type::state.status!2|)) 0)) (not (>= (+ (- 3) (* 1 |state_type::state.status!4|)) 0)) (not (>= (+ (- 3) (* 1 |state_type::state.status!1|)) 0)) (not (>= (* (- 1) |state_type::state.status!4|) 0)) (not (>= (+ (- 2) (* 1 |state_type::state.status!2|)) 0)) (not (>= (+ (- 2) (* 1 |state_type::state.status!1|)) 0)) (not (>= (* (- 1) |state_type::state.status!2|) 0)) (not (>= (+ (- 1) (* 1 |state_type::state.status!1|)) 0)) (not (>= (+ (- 2) (* 1 |state_type::state.status!4|)) 0)) (not (>= (+ (- 1) (* 1 |state_type::state.status!4|)) 0)) (not (>= (+ (- 1) (* 1 |state_type::state.status!2|)) 0)))
:named b))
(check-sat)
(get-interpolants a b)
(exit)
